package pap.test.fcPuGm;

import gov.nasa.jpf.jvm.Verify;

public class SynchronizedCounter {

	int maxVal;
	int count;

	public SynchronizedCounter(int maxVal) {
		Verify.beginAtomic();
		this.maxVal = maxVal;
		count = 0;
		Verify.endAtomic();
	}

	/**
	 * Returns and increments the actual value of the counter. Blocks if the
	 * value is equal to maxVal.
	 * 
	 * @return Value of the counter
	 * @throws InterruptedException
	 */
	public synchronized int getNextVal() throws InterruptedException {
		while (count >= maxVal)
			wait();
		return count++;

	}

	/**
	 * Reinitializes the max value to maxVal and the actual value to 0.
	 * 
	 * @param maxVal
	 */
	public synchronized void reset(int maxVal) {
		Verify.beginAtomic();
		this.maxVal = maxVal;
		count = 0;
		notifyAll();
		Verify.endAtomic();
	}
}
